- 程式語言是一種形式語言，作為思考的工具。我們用程式語言表達概念，也用程式語
言中的形式規則檢驗程式的正確性。領域不同、目的不同，適合的程式語言也不同。
一個語言如果不改變你的思考方式，就不值得學 (Alan Peris)。

- 只要定義出資料型態，很多程式都可用歸納法寫出。

- 好的型別系統常有只要型別對，程式就會對的特性。

- 型別系統與邏輯有密切關係。計算科學的發展也和數學/邏輯學界的潮流息息相關。

- 有良好性質的語言可用數學推衍確保正確性，甚至可以從 specification 把
程式「算」出來。

- 許多程式語言的特性，如傳值方式、變數範疇、lazy/eager evaluation 等等
的「意義」（語意）都可用數學方式描述。

- 如 C 之類的 imperative 語言之程式的正確性也可以證明。寫一個 imperative
程式的關鍵是迴圈不變量。